2014 ICCAD CAD Contest

Simultaneous CNF Encoder Optimization with SAT solver Setting Selection

Chih-Jen Hsu

Taiwan Cadence Design Systems, Inc.


*Update*: 10 benchmark cases have been released in the Testcase session.

*Update*: 4 benchmark cases have been released in the Testcase session.

1. Introdcution

Efficiently solving the combinational single-output netlist is an important core engine, which is widely and frequently used for conquering the modern front-end problems, such as logic rewriting, false path analysis, property checking, and equivalence checking. In practical usage, one application would solve numerous sub-problems where each sub-problem is formulated in a single-output netlist. Although the sub-problems may be varied in their structure and topology, they have similar circuit characteristics like: size, depth, and combinations. Although we cannot directly reuse the learnt data, we can rely on the learnt characteristic to optimize the solving process among the numerous sub-problems for reducing the total runtime. Besides, the runtime for solving a single-output function is decided by two factors: the CNF encoding [1-4,11] and the SAT solving [5]. If we can explore the best CNF encoding setting and the best SAT solver setting by the small set of sampled sub-problems, we can significantly reduce the total runtime for solving the numerous similar sub-problems. In this contest, we request the participant to write a program that explores the best setting of the CNF encoder and the SAT solver.

State-of-the-art SAT solvers [6] have smart decision and learning procedures [7-9] for dealing with the various applications by the set of global optimized parameters. However, these parameters are not the best for solving a particular SAT instance. Fortunately, in our practical experience, if the parameters are useful for one case, they would also be useful for cases with similar characteristics. This means, if we can explore the best setting, we can use it to guide the solver amongst the SAT instances in a problem or amongst the problems with the similar characteristics. In addition to the SAT solver setting, the CNF encoding for a netlist is an important factor that affects the solving process. Therefore, the good encoding and solver setting can guide the solving and significantly reduce the total runtime for solving all the sub-problems. Therefore, the industrial approach to using the SAT solver would have two phases: the setting exploration phase—to decide the best encoder and solver setting, and the solving phase—to solve numerous similar problems, based on the generated encoder and solver setting.

In this contest, in the setting exploration phase, we ask the participant to optimize the CNF encoding setting and the SAT solver setting simultaneously from the sampled sub-problems, called samples. In the solving phase, we will evaluate the quality of optimized settings on the remaining sub-problems, called tests. Therefore, the requested program should have two modes: in setting exploration phase, your program should optimize and generate the SAT solver setting and encoder setting based on the small set of samples, and in the solving phase, your program becomes a CNF encoder that converts a test into a CNF, based on your optimized setting. Furthermore, we will evaluate the solving runtime based on the solver setting and the generated CNF. The one that correctly solves the most tests within the shortest runtime will be recognized the best tool and win the contest.

2. Problem Description and Input/Output Format

Figure 1.

Figure 1. flow chart of the program requirement

Figure.1 shows the flow chart of the program requirements and the solving process for a case. Each case contains three samples and ten tests, where the sample and the test are the single-output combinational gate-level netlist in Verilog format. There are two phases for each case: the setting exploration phase and the solving phase for 10 tests (i.e. 1 time exploration, 10 times solving). In the exploration phase, your program should be in exploration mode. In the solving phase, your program is in generation mode and becomes a CNF encoder optimized by the encoder setting. Your program should be named ”expcnf” with two modes named ”-exp” for the exploration mode and ”-gen” for the generation mode. We explain the detailed description in the following paragraphs.

Notes: 10 testsare far from the real problem, but to ease evaluation we have limited it to just 10 tests for each case.
Only the output file we describe will be written out. The other files cannot be written out in both phases.

Setting Exploration Phase

In the setting exploration phase, the requested program is in exploration mode and accepts three samples and generates the solver setting and encoder setting within 1800 seconds. The program execution would be:

expcnf –exp <sample1.v> <sample2.v> <sample3.v> <EncoderSetting> <SATSolverSetting>

The encoder setting should be in a single file and can be any format that you define and contain any information you learned in the exploration phase. The SAT solver setting is a single line command in a file that specifies one solver with its arguments, like “solver_a -ccmin-mode=1” where solver_a is the chosen solver and -ccmin-mode=1 is the used argument.

The participant can only use one of the following solvers:

To be fair, we installed the listed solvers onto our evaluation machine and will base the evaluation on our compiled solvers. The input of our program is 3 samples. A sample must be in Verilog format and contains flattened, combinational gate-level netlist composed of only primitive gate.

Note: The solver here should contain only the executable binary name without the path.

Solving Phase

In each solving phase, the requested program is in generation mode and accepts the generated encoder setting file to convert a test into a satisfiable equivalence CNF file. The program execution would be:

expcnf –gen <EncoderSetting> <test.v> <CNF output>

The satisfiable equivalence CNF means:

The generated CNF is satisfiable if and only if the output of given netlist could be one.

The format of a test is the same as the sample in exploration mode, it is in Verilog format and contains flattened, combinational gate-level netlist composed of only primitive gate. The CNF file format is in DIMACS CNF format [10].

There are 10 tests in a case, in solving phase. For each case, it would generate 10 CNF files. We will solve each CNF file using the solver setting you generated in the exploration phase. For each test, the runtime of CNF generation is t1 and the runtime of SAT solving is t2. We calculate the cost using the function 4 × t1 + t2. We multiply 4 in runtime of CNF generation because we want the contest to focus on fast CNF generation. The program with the least total cost wins.

3. Example

Exploration phase:

Figure 2.

Solving phase:

Figure 3.

4. Language

5. Evaluation

We will select 2 open cases and 10 hidden cases for evaluation. Each case contains 3 samples for the exploration phase and 10 tests for the solving phase. Each case will have a cost value evaluated by the following process.

Exploration phase:

  1. The time limit for exploration phase is 1800 seconds. If it exceeds this time, we will not enter the solving phase and the cost for this case will be 3000. Otherwise, the cost is determined by the solving phase.

Solving phase:

  1. The results (SAT or UNSAT) return by the SAT engine should be correct. Otherwise, you will be disqualified.

  2. You will get a cost for each test according to the runtime of CNF generation ( t1 seconds) and the runtime for solving the CNF (t2 seconds). The cost is 4 × t1 + t2 only when t1 < 25 s and t2 < 100 s. Otherwise, the cost will be 300. The summation cost of 10 tests is the cost for this case.

If the results of all cases are correct, the summation cost of 12 cases is the total cost of your program. The program with least total cost wins.

6. Reference

  1. Niklas Eén, Alan Mishchenko, and Niklas Sörensson, "Applying Logic Synthesis for Speeding Up SAT", SAT 2007.

  2. Benjamin Chambers, Panagiotis Manolios, "Faster SAT Solving with Better CNF Generation", DATE 2009.

  3. Niklas Eén, Armin Biere, "Effective Preprocessing in SAT through Variable and Clause Elimination", SAT 2005.

  4. Marijn Heule, Matti Jarvisalo,and Armin Biere, "Clause Elimination Procedures for CNF Formulas", LPAR-17, 2010.

  5. Joao P. Marques Silva, Karem A. Sakallah, "GRASP-A New Search Algorithm for Satisfiability", ICCAD 1996.

  6. Niklas Eén, Niklas Sörensson, "An Extensible SAT-solver", SAT 2003.

  7. Matthew W. Moskewicz, C.F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik, "Chaff: Engineering an Efficient SAT Solver", DAC 2001.

  8. Jinbo Huang, "The Effect of Restarts on the Efficiency of Clause Learning", IJCAI 2007.

  9. Gilles Audemard, Laurent Simon, "Predicting Learnt Clauses Quality in Modern SAT Solvers", IJCAI 2009.

  10. DIMACS CNF format http://logic.pdmi.ras.ru/~basolver/dimacs.html

  11. M.N. Velev, Efficient Translation of Boolean Formulas to CNF in Formal Verification of Microprocessors, Asia and South Pacific Design Automation Conference (ASP-DAC '04), January 2004, pp. 310-315.

7. Q&A

  1. Are there any further information about the relation between sample and test designs?

    No, no further information we would provide, actually contestants would go to learn that.
  2. Would you mind list all types of gate belonging to primitive gates? And what is the maximum input pin number of the gates?

    Ok, we would go to provide them and also announce the maximum input number, but don’t worry about the abnormal case now.
  3. Which solver is used for solving optimized CNF file after solving phase? Could participant choose ideal solver for their encoding?

    Of course, you should specify the solver you want to used into the solver-setting file, which would be a executable line without cnf-file.
  4. At the third paragraph 'Example' solving phase. Is Input :verilog netlist mapping correctly to Output:CNF file?

    No, it’s the good question and important keypoint about this problem. You only need to consider about the satisfiable equivalence in your transformation.
  5. May I know whether multi-threading is allowed for the problem "Simultaneous CNF Encoder Optimization with SAT solver Setting Selection"? And, do we have to submit our source code? We would also like to know whether the system can execute binaries compiled in newer linux version (say the version of g++ is 4.6.3).

    We cannot use multi-threading for fairness. Please explain why you want to use this version (i.e 4.6.3), is there any special reason or library you want to use?. You can include all the library you need. Because for fairness, we cannot easily change our evaluation environment except there is problem defect.
  6. The link provided on the problem description website for minisat, http://minisat.se/downloads/minisat-2.2.0.tar.gz, appears to be a dead link. Actually, as far as I can tell, the entire minisat.se domain is down, and has been for at least the last three weeks. I have tried installing directly from Niklas Sörensson's github repository for the minisat project, but I'm receiving a weird dynamically linked library issue that I think is probably explained on the website :). Do you know anything about the website being down, and if it will return?

    Thanks for your notification, and we will go to use the version in github.
  7. Due to the number of output file is exactly one as the problem description, could we delete the others during the exploration and solving phase?

    No problem, you can generate any side files during the exploration phase and the solving phase. However, if you want to catch the learning information between exploration to solving phase, you should keep them all in “encoder setting file”. We would go to check and remove the side files among “run-by-run”, i.e. each time call “expcnf”
  8. Is there any contraints on the number of executable file "expcnf"? Could the problem be performed as problem description using multiple executable files?

    Right, we have no such constraints. However, if the executable file is not time-invariant, we would treat it as the “side-file”, and will remove them run-by-run.
  9. Since the linux system in the evaluation environment is pretty old, we are afraid that our program cannot be executed in that environment because of kernel incompatibility. Could you please advice on whether it is safe to use execvp() to execute the solvers installed in the system? Do we have to submit our source code?

    No problem you can use execvp. You don’t have to submit your source code.
  10. Is it possible to release the SAT/UNSAT results of all utx cases? The SAT-solvers take so much time solving the problems for obtaining the golden results for verification.

    We have no such planning. We encourage contestant to validate the CNF transformation with the general problems, such as SAT-race 2010 special track2 with 3rd party technology mapping.
  11. That was a question in Q&A mention that this contest can't use multi-threading for fairness. and i was use tool ABC berkeley(using multi-threading) and submit in alpha test then get grade, so is that really OK to use ABC in this contest?

    No problem to use ABC, Thanks.
  12. Does the evaluation and time out condition based on CPU time?

    It is wall time.
  13. We find that in the beta submission we used the word "lingeline" to run the program and it works. However, the website say that the name should be "lingeling". We want to make sure that if both names can work. Or we should use "lingeling" to run our program?

    Since we make the typo, so both names are acceptable.
  14. Why the costs on the website of ut2 in the alpha submission are better than that of the beta submission? Do they run in different work station?

    No, we do not change the machine, there are other reasons J, but we would not change the machine in Alpha, Beta, and final test.
  15. We'd like to use some tools during our CNF generation. Are we allowed to submit some perl files / executable files and call them within our main code during the generation phase?

    We do not forbid to call other tools. However, for setting the environment correctly, we would only link the script to some run directory.Please be sure to have an executable environment, that’s the purpose of alpha and beta test.

8. Testcases

  1. ut1.tgz
  2. ut2.tgz
  3. ut3.tgz
  4. ut5.tgz
  5. ut7.tgz
  6. ut8.tgz
  7. ut13.tgz
  8. ut14.tgz
  9. ut15.tgz
  10. ut20.tgz
  11. ut26.tgz
  12. ut32.tgz
  13. ut36.tgz
  14. ut41.tgz

9. Alpha test result

Cases Best result 2nd result 3rd result
cost of ut1 147.28 1315.6 1381.77
cost of ut2 637.28 758.06 799.18

10. Beta test result

Cases Best result 2nd result 3rd result
cost of ut1 55.7 521.67 552.15
cost of ut2 1070.25 1146.62 1156.39
cost of ut3 3000 3000 3000
cost of ut5 1643.63 1902.32 1906.79
cost of ut7 97.53 734.45 853.41
cost of ut8 228.58 1956.21 1973.68
cost of ut13 999.68 1542.88 1646.52
cost of ut14 3000 3000 3000
cost of ut15 2710.12 2765.44 3000
cost of ut20 2701.84 2705.72 2708.88
cost of ut26 3000 3000 3000
cost of ut32 1935.5 1974.21 2023.78
cost of ut36 2395.95 2401.03 2401.26
cost of ut41 3000 3000 3000

11. ICCAD 2014 contest result

Benchmarks for final evaluation

final_evaluation.tgz

Results of Top 3 teams

1. EasySat
2.
AlcomSAT
3.
Troller Coaster